T:Type, as,cs,bs,ds:(T List).
compat(T; append(as; bs); append(cs; ds))  (as = cs)  compat(T; bs; ds) 

latex

Definitions	t  T, compat(T; l1; l2), P  Q, x:A. B(x), append(as; bs), prop{i:l}, False, P  Q, P  Q, ||as||, ge(i; j), hd(l), A, A  B, tl(l), P  Q
Lemmas	tl wf, ge wf, hd wf, non neg length, length wf1, compat-cons, compat wf, append wf